1. $i$ : $\mathbb{Z}$ \\[0ex]2. $j$ : $\mathbb{Z}$ \\[0ex]$\vdash$ (($i$ =$_{0}$ $j$) $\sim$ tt) $\in$ Type